docs+fix: README.md → README.adoc, and fix broken Idris2 test suite (// → -- comments) - #46
Merged
Merged
Conversation
Per the estate docs standard, README is .adoc by default; only boj-server and the profile repo are the .md exceptions. julia-professional-registry is neither, so README.md was a prior-AI md-ification error. Converted to AsciiDoc and removed the .md (no duplicate formats). - Faithful conversion of Overview / Usage / the 37-package table / License. - Native AsciiDoc image badges (dropped the malformed <embed> green-web badge). - License section states MPL-2.0 (code) + CC-BY-SA-4.0 (docs), matching LICENSE and LICENSES/. - Title set to the canonical registry name (JuliaProfessionalRegistry). Render-validated with asciidoctor (--failure-level=WARN → 0 warnings; 37-package table intact). No V-lang/PMPL token; README.adoc at repo root.
Ground-truthed with a locally-built idris2 0.7.0: `idris2 --build julia-professional-registry-tests.ipkg` failed with "Couldn't parse declaration" at ValidateTest.idr:2. Cause: line 2 of all three test modules (Main.idr, Test/Spec.idr, ValidateTest.idr) used a C/Zig-style `// Owner: ...` comment, but Idris2 comments are `--`. A prior header sweep applied the wrong comment syntax to the Idris2 files. Fixed `//` → `--` on those lines. Verified: the suite now builds cleanly (idris2 --build exit 0; all 3 modules typecheck + the executable compiles). Companion ground-truth (no change needed): Axiom's axiom-abi.ipkg and julianiser's julianiser-abi.ipkg both already typecheck — their .idr were sound, just never checked in CI (G05 / G34: the fix there is to ADD an idris2 --build gate, tracked separately).
hyperpolymath
marked this pull request as ready for review
July 1, 2026 20:40
hyperpolymath
enabled auto-merge (squash)
July 1, 2026 20:40
hyperpolymath
disabled auto-merge
July 1, 2026 21:02
hyperpolymath
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Two registry corrections (GitHub MCP was briefly down, so both landed on one branch):
.md→.adoc(estate.adoc-default docs policy; onlyboj-server+ the profile repo are.mdexceptions). Faithful conversion of Overview / Usage / the 37-package table / License; native AsciiDoc badges;README.mddeleted.idris2 --build julia-professional-registry-tests.ipkgfailed with "Couldn't parse declaration" atValidateTest.idr:2. All three test modules (Main,Test/Spec,ValidateTest) had a C/Zig-style// Owner:comment on line 2, but Idris2 comments are--(a prior header sweep used the wrong syntax). Fixed//→--.Verification
asciidoctor --failure-level=WARN README.adoc→ 0 warnings; 37-package table renders.idris2 --build julia-professional-registry-tests.ipkg→ exit 0: all 3 modules typecheck + the executable compiles (was previously a hard parse error).RSR Quality Checklist
Required
As Applicable
cartridge.json/registry-index change🤖 Generated with Claude Code